$\forall$$T$:Type, $R$:($T$$\rightarrow$$T$$\rightarrow\mathbb{P}$). connex($T$;$R$$^{\circ}$) $\Leftarrow\!\Rightarrow$ ($\forall$$a$, $b$:$T$. ($R$($a$,$b$)) $\vee$ ($a$ = $b$) $\vee$ ($R$($b$,$a$)))